package projeto;

public interface Grafo {
	
	//@ public model instance int _contvertices;
	//@ public model instance int _contArestas;
	//@ public model instance int _tamanho;
	//@ public model instance Aresta[] _listaArestas;
	
	/*@ public normal_behavior
	 @		requires _contvertices < _tamanho;
	 @		assignable _contvertices;
	 @	    ensures _contvertices == \old(_contvertices) + 1; 	 
	 @ also
	 @	public exceptional_behavior
	 @		requires _contvertices >= _tamanho;
	 @		assignable \nothing;
	 @		signals_only GrafocheioException;
	 @*/
	public void inserirVertice(Vertice v) throws VerticeDuplicadoException, GrafocheioException;
	
	public /*@ pure @*/ Aresta[] getArestas();
	
	public /*@ pure @*/ Aresta[] getArestasIncidentes(Vertice v) throws VerticeInvalidoException;
	 
	public /*@ pure @*/ Vertice getVertice(String nome);
	
	//@ ensures \result == _contArestas;
	public /*@ pure @*/ int getNumeroArestas();
	
	//@ ensures \result == _contvertices;
	public /*@ pure @*/ int getNumeroVertices();
	
	public /*@ pure @*/ Vertice[] getVerticesAdjacentes(Vertice v) throws VerticeInvalidoException;
	
	public /*@ pure @*/ Aresta get_Aresta(Vertice in, Vertice fi) throws VerticeInvalidoException, AmbosVerticesInexistentesException;

	public void inserirAresta(Aresta a) throws VerticeInvalidoException,
			AmbosVerticesInexistentesException;

	public void removerAresta(Vertice vi, Vertice vf) throws AmbosVerticesInexistentesException,VerticeInvalidoException;

}
